package alloy.api;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.StringTokenizer;
import java.util.TreeSet;

import javax.swing.JFrame;

import alloy.util.Dbg;
import alloy.viz.gui.VizPanel;

public class AlloyTextInterface {
    private static Dbg.DbgMsgListener msgListener = new Dbg.DbgMsgStreamPrinter(System.out);

    private static AlloyController controller = null;

    private static Map operMap;

    public static void main(String args[]) {
    Dbg.addDbgMsgListener(Dbg.USER, msgListener);

    String command = null;

    operMap = new HashMap();
    operMap.put("load", loadFileOp);
    operMap.put("read", readModelOp);
    operMap.put("show", showModelOp);
    operMap.put("build", buildOp);
    operMap.put("exec", executeOp);
    operMap.put("lc", listCommandsOp);
    operMap.put("view", viewSolutionOp);
    operMap.put("count", countSolutionsOp);
    operMap.put("next", nextOp);
    operMap.put("abort", abortOp);
    operMap.put("status", printStatusOp);
    operMap.put("set", setOptionOp);
    operMap.put("get", getOptionOp);
    operMap.put("getall", getAllOptionsOp);
    operMap.put("viz", visualizeOp);
    operMap.put("file", currentFileOp);
    operMap.put("help", helpOp);
    operMap.put("quit", quitOp);
    operMap.put("eval", evalExprOp);

    while (true) {
        System.out.print("ALLOY> ");
        command = readLine();
        evaluate(command);
    }
    }

    private static void evaluate(String command) {
    if (command == null)
        return;

    StringTokenizer st = new StringTokenizer(command);

    if (!st.hasMoreTokens())
        return;

    String opName = st.nextToken();
    Operation op = (Operation)operMap.get(opName);

    if (op != null) {
        if ((op.numArgs() < 0) || (st.countTokens() == op.numArgs())) {
        op.perform(st);
        } else {
        System.out.println("Wrong arguments to command: " + opName);
        }
    } else {
        System.out.println("Invalid command: " + opName);
    }
    }

    private static String readLine() {
    BufferedReader in = new BufferedReader(new InputStreamReader(System.in));
    String s = null;

    try {
        s = in.readLine();
    } catch (IOException e) {}
    return s;
    }

    private static void printAhead(String s) {
    int i;
    for (i = 0; i < 30; i++) {
        System.out.print(" ");
    }

    System.out.print(s);

    for (i = 0; i < s.length() + 30; i++) {
        System.out.print("\u0008");
    }
    }

    abstract static class Operation {
    private int numArgs;
    /**
     * Negative <code>numArgs</code>
     * designates an arbitrary number of arguments
     * to this Operation.
     **/
    Operation(int numArgs_) {
        numArgs = numArgs_;
    }

    abstract public void perform(StringTokenizer st);

    public int numArgs() {
        return numArgs;
    }
    }

    private static final Operation evalExprOp = new Operation(-1) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            Dbg.user("no model loaded");
            return;
        }

        String expr = "";
        while (st.hasMoreTokens()) {
            expr += st.nextToken() + " ";
        }
        Dbg.removeDbgMsgListener(Dbg.USER, msgListener);
        String res = controller.evaluateExpr(expr);
        System.out.println(res);
        Dbg.addDbgMsgListener(Dbg.USER, msgListener);
        }
    };

    private static final Operation loadFileOp = new Operation(1) {
        public void perform(StringTokenizer st) {
        String filePath = st.nextToken();
        try {
            controller = new AlloyController(new File(filePath));
            System.out.println("File loaded successfully.");
        } catch (Exception e) {
            System.out.println("Cannot read from file: " + filePath);
        }
        }
    };

    private static final Operation readModelOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        String model = "";
        String line = readLine();
        while (line != null) {
            model = model + line + "\n";
            line = readLine();
        }
        controller = new AlloyController(model);
        }
    };

    private static final Operation showModelOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            System.out.print(controller.getModel());
        }
        }
    };

    private static final Operation quitOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        System.exit(0);
        }
    };

    private static final Operation buildOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            try {
            controller.build(new AlloyController.ThreadFinisher() {
                public void threadFinished(Object success) {
                    if (((Boolean)success).booleanValue()) {
                    printAhead("*** BUILD SUCCEEDED ***");
                    } else {
                    printAhead("!!! BUILD FAILED !!!");
                    }
                }
                });
            } catch (UnavailableOperationException e) {
            System.out.println("Operation not available.");
            }
        }
        }
    };

    private static final Operation listCommandsOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            try {
            List commands = controller.allCommandInfos();

            if (commands.isEmpty()) {
                System.out.println("No commands have been defined.");
            } else {
                Iterator i = commands.iterator();
                int count = 1;
                int index = controller.getCommandIndex();
                while (i.hasNext()) {
                System.out.println((index == count ? "*" : "") +
                           count +
                           ") " + i.next());
                count++;
                }
            }
            } catch (UnavailableOperationException e) {
            System.out.println("Operation not available.");
            }
        }
        }
    };

    private static final Operation executeOp = new Operation(1) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            try {
            int index = Integer.parseInt(st.nextToken());

            if (index < 1 || index > controller.numCommands()) {
                System.out.println("Invalid command number.");
            } else {
                controller.setCommand(index);
                final long start = System.currentTimeMillis();
                controller.execute(new
                AlloyController.ThreadFinisher() {

                    public void threadFinished(Object success) {
                      long finish = System.currentTimeMillis();

                      if (((Boolean)success).booleanValue()) {
                        if (controller.getInstance() != null) {
                          printAhead("*** SOLUTION FOUND ***");
                        } else {
                          printAhead("*** NO SOLUTION FOUND ***");
                        }
                      } else {
                        printAhead("!!! SOLVE ABORTED !!!");
                      }

                      double seconds = (finish - start) / 1000.0;
                      System.out.println();
                      printAhead(seconds + " seconds");
                    }
                });
            }
            } catch (NumberFormatException e) {
              System.out.println("Invalid command number.");
            } catch (UnavailableOperationException e) {
              System.out.println("Operation not available.");
            }
        }
        }
    };

    private static final Operation abortOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("Nothing to abort.");
        } else {
            try {
            controller.abort();
            } catch (UnavailableOperationException e) {
            System.out.println("Nothing to abort.");
            }
        }
        }
    };

    private static final Operation viewSolutionOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else if (controller.getInstance() == null) {
            System.out.println("No solution currently found.");
        } else {
            System.out.println(controller.getInstance());
        }
        }
    };

    private static final Operation countSolutionsOp = new Operation(1) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            if (!controller.countingSolverSelected()) {
            System.out.println("MAIN.solver must be set to RELSAT to enable counting");
            } else try {
            int index = Integer.parseInt(st.nextToken());

            if (index < 1 || index > controller.numCommands()) {
                System.out.println("Invalid command number.");
            } else {
                controller.setCommand(index);

                controller.countSolutions(new
                AlloyController.ThreadFinisher() {
                    public void threadFinished(Object count) {
                    if (count == null) {
                        printAhead("!!! COUNT ABORTED !!!");
                    } else {
                        printAhead("*** COUNT SUCCEEDED: " +
                               count +
                               " solutions found ***");
                    }
                    }
                });
            }
            } catch (NumberFormatException e) {
            System.out.println("Invalid command number.");
            } catch (UnavailableOperationException e) {
            System.out.println("Operation not available.");
            }
        }
        }
    };

    private static final Operation nextOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else {
            try {
            controller.next(new
                AlloyController.ThreadFinisher() {
                public void threadFinished(Object success) {
                    if (((Boolean)success).booleanValue()) {
                    if (controller.getInstance() != null) {
                        printAhead("*** SOLUTION FOUND ***");
                    } else {
                        printAhead("*** NO SOLUTION FOUND ***");
                    }
                    } else {
                    printAhead("!!! SOLVE ABORTED !!!");
                    }
                }
                });
            } catch (UnavailableOperationException e) {
            System.out.println("Operation not available.");
            }
        }
        }
    };

    private static final Operation printStatusOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null ||
            controller.getRunStatus() == AlloyController.AVAILABLE) {
            System.out.println("No computation in progress.");
        } else if (controller.getRunStatus() ==
               AlloyController.BUILD_IN_PROGRESS) {
            System.out.println("Build in progress.");
        } else if (controller.getRunStatus() ==
               AlloyController.SOLVE_IN_PROGRESS) {
            System.out.println("Solve in progress.");
        } else if (controller.getRunStatus() ==
               AlloyController.COUNT_IN_PROGRESS) {
            System.out.println("Count in progress.");
        } else {
            // should not happen
        }
        }
    };

    public static final Operation setOptionOp = new Operation(3) {
        public void perform(StringTokenizer st) {
        String grpName = st.nextToken();
        String paramName = st.nextToken();
        String value = st.nextToken();

        AlloyController.setOption(grpName, paramName, value);
        }
    };

    public static final Operation getOptionOp = new Operation(2) {
        public void perform(StringTokenizer st) {
        String grpName = st.nextToken();
        String paramName = st.nextToken();

        System.out.println(grpName + "." + paramName + " = " +
                   AlloyController.getOption(grpName, paramName));
        }
    };

    public static final Operation getAllOptionsOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        System.out.print(AlloyController.getAllOptions());
        }
    };

    public static final Operation visualizeOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null || controller.getInstance() == null) {
            System.out.println("No solution currently found.");
        } else {
            System.out.println("Opening new window...");

            JFrame f = new JFrame("Alloy Visualization");
            VizPanel p = new VizPanel(controller.getInstance().getVizInstance(),
                          new alloy.api.AlloyEvaluator(controller.getInstance()));
            f.getContentPane().add(p);

            int sw = alloy.gui.AlloySwingUtilities.getScreenWidth();
            int sh = alloy.gui.AlloySwingUtilities.getScreenHeight();
            f.setBounds(sw/4,sh/4,sw/2,sh/2);
            f.show();
        }
        }
    };

    public static final Operation helpOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        // get list of commands in alphabetical order
        Iterator i = new TreeSet(operMap.keySet()).iterator();

        while (i.hasNext()) {
            System.out.println(i.next());
        }
        }
    };

    public static final Operation currentFileOp = new Operation(0) {
        public void perform(StringTokenizer st) {
        if (controller == null) {
            System.out.println("No Alloy model loaded.");
        } else if (controller.getFilePath() == null) {
            System.out.println("Current model not saved.");
        } else {
            System.out.println(controller.getFilePath());
        }
        }
    };
}
